Search for: All records

In this paper, we consider the verification of approximate infinite-step opacity for discrete-time control sys-tems. Relying on finite abstraction techniques for solving this problem requires discretization of the state and input sets, which requires significant computational resources. Here, we propose a discretization-free approach in which we formulate opacity as a safety property over an appropriately constructed augmented system, and seek to verify it by finding suitable barrier certificates. Within our proposed scheme, lack of opacity is also verified by posing it as a reachability property over the augmented system. The main result of this paper offers a discretization-free approach to verify (lack of) infinite-step opacity in discrete-time control systems. We also discuss other notions of opacity, and their relations to one another. We particularly study the conditions under which verifying one form of opacity for a system also implies other forms. Finally, we illustrate our theoretical results on two numerical examples, where we utilize sum-of-squares programming to search for polynomial barrier certificates. In these examples, we verify the infinite-step, and current-step opacity for a vehicle by checking whether its position is concealed from possible outside intruders.